\begin{abstract}
Maude is a declarative and reflective language based on rewriting
logic in which computation corresponds to efficient deduction by
rewriting. Because of its reflective capabilities, Maude has been
useful as a {\em metatool}
in the development of formal analysis tools for checking
specific properties of Maude specifications.
This includes tools for checking termination, confluence, and inductive
properties of rewrite theories. 
Nevertheless, most of these tools have been designed to work
in isolation, making it difficult, for instance, to exchange data between
them and inconvenient to switch between their environments.
This paper presents the Maude Formal Environment (MFE), 
an executable formal specification in Maude within which a 
user can interact with tools to mechanically verify 
properties of Maude specifications. 
One important aspect of this work is that the MFE 
has been designed to be easily extended with
tools having highly heterogeneous designs whilst creating
synergy among them. As a proof of concept,
we report on the integration of five 
commonly used formal analysis tools for Maude specifications into MFE
and illustrate their interoperability with an example.

%Besides giving support to exchange data among tools and
%to easily switch between their environments,\mnote{I whole emphasize on the interaction between the tools and in the holistic use in the environment (in the sense that they working together represents more than their sum.} 
%MFE also provides a new mechanism
%for recording user sessions\mnote{for me this is less relevant} and for maintaining 
%several instances of tools\mnote{I should leave this for the body of the paper as well}.

\end{abstract}
